home *** CD-ROM | disk | FTP | other *** search
/ NetNews Offline 2 / NetNews Offline Volume 2.iso / news / comp / lang / c-part1 / 8632 < prev    next >
Encoding:
Internet Message Format  |  1996-08-05  |  1.3 KB
  1. Path: keats.ugrad.cs.ubc.ca!not-for-mail
  2. From: c2a192@ugrad.cs.ubc.ca (Kazimir Kylheku)
  3. Newsgroups: comp.lang.c
  4. Subject: Re: Formal type system and denotational semantics for C?
  5. Date: 5 Mar 1996 07:27:56 -0800
  6. Organization: Computer Science, University of B.C., Vancouver, B.C., Canada
  7. Message-ID: <4hhmhsINNqcj@keats.ugrad.cs.ubc.ca>
  8. References: <313C52B1.41C67EA6@cs.wisc.edu>
  9. NNTP-Posting-Host: keats.ugrad.cs.ubc.ca
  10.  
  11. In article <313C52B1.41C67EA6@cs.wisc.edu>,
  12. Michael Siff  <siff@cs.wisc.edu> wrote:
  13.  >Is anyone aware of any work done for either a formal type system for C
  14.  >or denotational semantics for C? I am particularly interested in the
  15.  >type question. I am looking for type rules of the form:
  16.  >
  17.  >A |- e : t
  18.  >-----------
  19.  >A |- &e : t ptr
  20.  >
  21.  >meaning: if with assumptions A (i.e. declarations and initial
  22.  >environment) expression e has type t, then &e has type pointer to t.
  23.  >
  24.  >Any information concerning the existence of such rules would be much
  25.  >appreciated. 
  26.  
  27. There is the ANSI/ISO standard, but which doesn't go into this level of
  28. formalism. It's quite a human-readable document. :) It does state _some_ things
  29. formally using grammar notation to define the syntax of the language, but you
  30. are asking for all kinds of semantic notions to be codified also.
  31. -- 
  32.  
  33.